home *** CD-ROM | disk | FTP | other *** search
open in: 
MacOS 8.1
|
Win98
|
DOS
browse contents |
view JSON data
|
view as text
This file was processed as: LaTeX Document
(document/latex).
| Confidence | Program | Detection | Match Type | Support
|
|---|
| 100%
| dexvert
| LaTeX Document (document/latex)
| magic
| Supported |
| 1%
| dexvert
| Corel 10 Texture (image/corel10Texture)
| ext
| Unsupported |
| 1%
| dexvert
| Croteam texture file (image/croteamTextureFile)
| ext
| Unsupported |
| 1%
| dexvert
| Text File (text/txt)
| fallback
| Supported |
| 100%
| file
| LaTeX document text
| default
| |
| 99%
| file
| LaTeX auxiliary file, ASCII text
| default
| |
| 100%
| checkBytes
| Printable ASCII
| default
| |
| 100%
| perlTextCheck
| Likely Text (Perl)
| default
| |
| 100%
| detectItEasy
| Format: plain text[LF]
| default (weak)
|
|
hex view+--------+-------------------------+-------------------------+--------+--------+
|00000000| 5c 6d 65 73 73 61 67 65 | 7b 3c 50 61 75 6c 20 54 |\message|{<Paul T|
|00000010| 61 79 6c 6f 72 27 73 20 | 50 72 6f 6f 66 20 54 72 |aylor's |Proof Tr|
|00000020| 65 65 73 2c 20 31 37 20 | 41 75 67 75 73 74 20 31 |ees, 17 |August 1|
|00000030| 39 39 30 3e 7d 0a 25 25 | 20 42 75 69 6c 64 20 70 |990>}.%%| Build p|
|00000040| 72 6f 6f 66 20 74 72 65 | 65 20 66 6f 72 20 4e 61 |roof tre|e for Na|
|00000050| 74 75 72 61 6c 20 44 65 | 64 75 63 74 69 6f 6e 2c |tural De|duction,|
|00000060| 20 53 65 71 75 65 6e 74 | 20 43 61 6c 63 75 6c 75 | Sequent| Calculu|
|00000070| 73 2c 20 65 74 63 2e 0a | 25 25 20 57 49 54 48 20 |s, etc..|%% WITH |
|00000080| 53 48 4f 52 54 45 4e 49 | 4e 47 20 4f 46 20 50 52 |SHORTENI|NG OF PR|
|00000090| 4f 4f 46 20 52 55 4c 45 | 53 21 0a 25 25 20 50 61 |OOF RULE|S!.%% Pa|
|000000a0| 75 6c 20 54 61 79 6c 6f | 72 2c 20 62 65 67 75 6e |ul Taylo|r, begun|
|000000b0| 20 31 30 20 4f 63 74 20 | 31 39 38 39 0a 25 25 20 | 10 Oct |1989.%% |
|000000c0| 2a 2a 2a 20 54 48 49 53 | 20 49 53 20 4f 4e 4c 59 |*** THIS| IS ONLY|
|000000d0| 20 41 20 50 52 45 4c 49 | 4d 49 4e 41 52 59 20 56 | A PRELI|MINARY V|
|000000e0| 45 52 53 49 4f 4e 20 41 | 4e 44 20 54 48 49 4e 47 |ERSION A|ND THING|
|000000f0| 53 20 4d 41 59 20 43 48 | 41 4e 47 45 21 20 2a 2a |S MAY CH|ANGE! **|
|00000100| 2a 0a 25 25 0a 25 25 09 | 5c 70 72 6f 6f 66 74 72 |*.%%.%%.|\prooftr|
|00000110| 65 65 0a 25 25 09 09 68 | 79 70 31 09 09 70 72 6f |ee.%%..h|yp1..pro|
|00000120| 64 75 63 65 73 3a 0a 25 | 25 09 09 68 79 70 32 0a |duces:.%|%..hyp2.|
|00000130| 25 25 09 09 68 79 70 33 | 09 09 68 79 70 31 09 68 |%%..hyp3|..hyp1.h|
|00000140| 79 70 32 09 68 79 70 33 | 0a 25 25 09 5c 6a 75 73 |yp2.hyp3|.%%.\jus|
|00000150| 74 69 66 69 65 73 09 09 | 2d 2d 2d 2d 2d 2d 2d 2d |tifies..|--------|
|00000160| 2d 2d 2d 2d 2d 2d 2d 2d | 2d 2d 2d 2d 20 72 75 6c |--------|---- rul|
|00000170| 65 6e 61 6d 65 0a 25 25 | 09 09 63 6f 6e 63 6c 09 |ename.%%|..concl.|
|00000180| 09 09 63 6f 6e 63 6c 0a | 25 25 09 5c 74 68 69 63 |..concl.|%%.\thic|
|00000190| 6b 6e 65 73 73 3d 30 2e | 30 38 65 6d 0a 25 25 09 |kness=0.|08em.%%.|
|000001a0| 5c 73 68 69 66 74 72 69 | 67 68 74 20 32 65 6d 0a |\shiftri|ght 2em.|
|000001b0| 25 25 09 5c 75 73 69 6e | 67 0a 25 25 09 09 72 75 |%%.\usin|g.%%..ru|
|000001c0| 6c 65 6e 61 6d 65 0a 25 | 25 09 5c 65 6e 64 70 72 |lename.%|%.\endpr|
|000001d0| 6f 6f 66 74 72 65 65 0a | 25 25 0a 25 25 20 77 68 |ooftree.|%%.%% wh|
|000001e0| 65 72 65 20 74 68 65 20 | 68 79 70 6f 74 68 65 73 |ere the |hypothes|
|000001f0| 65 73 20 6d 61 79 20 62 | 65 20 73 69 6d 69 6c 61 |es may b|e simila|
|00000200| 72 20 73 74 72 75 63 74 | 75 72 65 73 20 6f 72 20 |r struct|ures or |
|00000210| 6a 75 73 74 20 66 6f 72 | 6d 75 6c 61 65 2e 0a 25 |just for|mulae..%|
|00000220| 25 0a 25 25 20 54 6f 20 | 67 65 74 20 61 20 76 65 |%.%% To |get a ve|
|00000230| 72 74 69 63 61 6c 20 73 | 74 72 69 6e 67 20 6f 66 |rtical s|tring of|
|00000240| 20 64 6f 74 73 20 69 6e | 73 74 65 61 64 20 6f 66 | dots in|stead of|
|00000250| 20 74 68 65 20 70 72 6f | 6f 66 20 72 75 6c 65 2c | the pro|of rule,|
|00000260| 20 64 6f 0a 25 25 0a 25 | 25 09 5c 70 72 6f 6f 66 | do.%%.%|%.\proof|
|00000270| 74 72 65 65 09 09 09 77 | 68 69 63 68 20 70 72 6f |tree...w|hich pro|
|00000280| 64 75 63 65 73 3a 0a 25 | 25 09 09 5b 68 79 70 5d |duces:.%|%..[hyp]|
|00000290| 0a 25 25 09 5c 75 73 69 | 6e 67 09 09 09 09 09 5b |.%%.\usi|ng.....[|
|000002a0| 68 79 70 5d 0a 25 25 09 | 09 6e 61 6d 65 09 09 09 |hyp].%%.|.name...|
|000002b0| 09 20 20 2e 0a 25 25 09 | 5c 70 72 6f 6f 66 64 6f |. ..%%.|\proofdo|
|000002c0| 74 73 65 70 61 72 61 74 | 69 6f 6e 3d 31 2e 32 65 |tseparat|ion=1.2e|
|000002d0| 78 09 09 20 20 2e 6e 61 | 6d 65 0a 25 25 09 5c 70 |x.. .na|me.%%.\p|
|000002e0| 72 6f 6f 66 64 6f 74 6e | 75 6d 62 65 72 3d 34 09 |roofdotn|umber=4.|
|000002f0| 09 09 20 20 2e 0a 25 25 | 09 5c 6c 65 61 64 73 74 |.. ..%%|.\leadst|
|00000300| 6f 09 09 09 09 20 20 2e | 0a 25 25 09 09 63 6f 6e |o.... .|.%%..con|
|00000310| 63 6c 09 09 09 09 63 6f | 6e 63 6c 0a 25 25 09 5c |cl....co|ncl.%%.\|
|00000320| 65 6e 64 70 72 6f 6f 66 | 74 72 65 65 0a 25 25 0a |endproof|tree.%%.|
|00000330| 25 25 20 57 69 74 68 69 | 6e 20 61 20 70 72 6f 6f |%% Withi|n a proo|
|00000340| 66 74 72 65 65 2c 20 5c | 5b 20 61 6e 64 20 5c 5d |ftree, \|[ and \]|
|00000350| 20 6d 61 79 20 62 65 20 | 75 73 65 64 20 69 6e 73 | may be |used ins|
|00000360| 74 65 61 64 20 6f 66 20 | 5c 70 72 6f 6f 66 74 72 |tead of |\prooftr|
|00000370| 65 65 20 61 6e 64 0a 25 | 25 20 5c 65 6e 64 70 72 |ee and.%|% \endpr|
|00000380| 6f 6f 66 74 72 65 65 3b | 20 74 68 69 73 20 69 73 |ooftree;| this is|
|00000390| 20 6e 6f 74 20 70 65 72 | 6d 69 74 74 65 64 20 61 | not per|mitted a|
|000003a0| 74 20 74 68 65 20 6f 75 | 74 65 72 20 6c 65 76 65 |t the ou|ter leve|
|000003b0| 6c 20 62 65 63 61 75 73 | 65 20 69 74 0a 25 25 20 |l becaus|e it.%% |
|000003c0| 63 6f 6e 66 6c 69 63 74 | 73 20 77 69 74 68 20 4c |conflict|s with L|
|000003d0| 61 54 65 58 2e 20 41 6c | 73 6f 2c 0a 25 25 09 5c |aTeX. Al|so,.%%.\|
|000003e0| 4a 75 73 74 69 66 69 65 | 73 0a 25 25 20 70 72 6f |Justifie|s.%% pro|
|000003f0| 64 75 63 65 73 20 61 20 | 64 6f 75 62 6c 65 20 6c |duces a |double l|
|00000400| 69 6e 65 2e 20 49 6e 20 | 4c 61 54 65 58 20 79 6f |ine. In |LaTeX yo|
|00000410| 75 20 63 61 6e 20 75 73 | 65 20 5c 62 65 67 69 6e |u can us|e \begin|
|00000420| 7b 70 72 6f 6f 66 74 72 | 65 65 7d 20 61 6e 64 0a |{prooftr|ee} and.|
|00000430| 25 25 20 5c 65 6e 64 7b | 70 72 6f 6f 74 72 65 65 |%% \end{|prootree|
|00000440| 7d 20 61 74 20 74 68 65 | 20 6f 75 74 65 72 20 6c |} at the| outer l|
|00000450| 65 76 65 6c 20 28 68 6f | 77 65 76 65 72 20 74 68 |evel (ho|wever th|
|00000460| 69 73 20 77 69 6c 6c 20 | 6e 6f 74 20 77 6f 72 6b |is will |not work|
|00000470| 20 66 6f 72 20 74 68 65 | 20 69 6e 6e 65 72 0a 25 | for the| inner.%|
|00000480| 25 20 6c 65 76 65 6c 73 | 2c 20 62 75 74 20 69 6e |% levels|, but in|
|00000490| 20 61 6e 79 20 63 61 73 | 65 20 77 68 79 20 77 6f | any cas|e why wo|
|000004a0| 75 6c 64 20 79 6f 75 20 | 77 61 6e 74 20 74 6f 20 |uld you |want to |
|000004b0| 62 65 20 73 6f 20 76 65 | 72 62 6f 73 65 3f 29 2e |be so ve|rbose?).|
|000004c0| 0a 25 25 0a 25 25 20 41 | 6c 6c 20 6f 66 20 6f 66 |.%%.%% A|ll of of|
|000004d0| 20 74 68 65 20 6b 65 79 | 77 6f 72 64 73 20 65 78 | the key|words ex|
|000004e0| 63 65 70 74 20 5c 70 72 | 6f 6f 66 74 72 65 65 20 |cept \pr|ooftree |
|000004f0| 61 6e 64 20 5c 65 6e 64 | 70 72 6f 6f 66 74 72 65 |and \end|prooftre|
|00000500| 65 20 61 72 65 20 6f 70 | 74 69 6f 6e 61 6c 0a 25 |e are op|tional.%|
|00000510| 25 20 61 6e 64 20 6d 61 | 79 20 61 70 70 65 61 72 |% and ma|y appear|
|00000520| 20 69 6e 20 61 6e 79 20 | 6f 72 64 65 72 2e 20 54 | in any |order. T|
|00000530| 68 65 79 20 6d 61 79 20 | 61 6c 73 6f 20 62 65 20 |hey may |also be |
|00000540| 63 6f 6d 62 69 6e 65 64 | 20 69 6e 20 5c 6e 65 77 |combined| in \new|
|00000550| 63 6f 6d 6d 61 6e 64 27 | 73 0a 25 25 20 65 67 20 |command'|s.%% eg |
|00000560| 22 5c 64 65 66 5c 43 75 | 74 7b 5c 75 73 69 6e 67 |"\def\Cu|t{\using|
|00000570| 5c 73 66 20 63 75 74 5c | 74 68 69 63 6b 6e 65 73 |\sf cut\|thicknes|
|00000580| 73 2e 30 38 65 6d 5c 6a | 75 73 74 69 66 69 65 73 |s.08em\j|ustifies|
|00000590| 7d 22 20 77 69 74 68 20 | 74 68 65 20 61 62 62 72 |}" with |the abbr|
|000005a0| 65 76 69 61 74 69 6f 6e | 0a 25 25 20 22 5c 70 72 |eviation|.%% "\pr|
|000005b0| 6f 6f 66 74 72 65 65 20 | 68 79 70 31 20 68 79 70 |ooftree |hyp1 hyp|
|000005c0| 32 20 5c 43 75 74 20 5c | 63 6f 6e 63 6c 20 5c 65 |2 \Cut \|concl \e|
|000005d0| 6e 64 70 72 6f 6f 66 74 | 72 65 65 22 2e 20 54 68 |ndprooft|ree". Th|
|000005e0| 69 73 20 69 73 20 72 65 | 63 6f 6d 6d 65 6e 64 65 |is is re|commende|
|000005f0| 64 20 61 6e 64 0a 25 25 | 20 73 6f 6d 65 20 73 74 |d and.%%| some st|
|00000600| 61 6e 64 61 72 64 20 61 | 62 62 72 65 76 69 61 74 |andard a|bbreviat|
|00000610| 69 6f 6e 73 20 77 69 6c | 6c 20 62 65 20 66 6f 75 |ions wil|l be fou|
|00000620| 6e 64 20 61 74 20 74 68 | 65 20 65 6e 64 20 6f 66 |nd at th|e end of|
|00000630| 20 74 68 69 73 20 66 69 | 6c 65 2e 0a 25 25 0a 25 | this fi|le..%%.%|
|00000640| 25 20 5c 74 68 69 63 6b | 6e 65 73 73 20 73 70 65 |% \thick|ness spe|
|00000650| 63 69 66 69 65 73 20 74 | 68 65 20 62 72 65 61 64 |cifies t|he bread|
|00000660| 74 68 20 6f 66 20 74 68 | 65 20 72 75 6c 65 20 69 |th of th|e rule i|
|00000670| 6e 20 61 6e 79 20 75 6e | 69 74 73 2c 20 61 6c 74 |n any un|its, alt|
|00000680| 68 6f 75 67 68 0a 25 25 | 20 66 6f 6e 74 2d 72 65 |hough.%%| font-re|
|00000690| 6c 61 74 69 76 65 20 75 | 6e 69 74 73 20 73 75 63 |lative u|nits suc|
|000006a0| 68 20 61 73 20 22 65 78 | 22 20 6f 72 20 22 65 6d |h as "ex|" or "em|
|000006b0| 22 20 61 72 65 20 70 72 | 65 66 65 72 61 62 6c 65 |" are pr|eferable|
|000006c0| 2e 0a 25 25 20 49 74 20 | 6d 61 79 20 6f 70 74 69 |..%% It |may opti|
|000006d0| 6f 6e 61 6c 6c 79 20 62 | 65 20 66 6f 6c 6c 6f 77 |onally b|e follow|
|000006e0| 65 64 20 62 79 20 22 3d | 22 2e 0a 25 25 20 5c 70 |ed by "=|"..%% \p|
|000006f0| 72 6f 6f 66 72 75 6c 65 | 62 72 65 61 64 74 68 3d |roofrule|breadth=|
|00000700| 2e 30 38 65 6d 20 6f 72 | 20 5c 73 65 74 6c 65 6e |.08em or| \setlen|
|00000710| 67 74 68 5c 70 72 6f 6f | 66 72 75 6c 65 62 72 65 |gth\proo|frulebre|
|00000720| 61 64 74 68 7b 2e 30 38 | 65 6d 7d 20 6d 61 79 20 |adth{.08|em} may |
|00000730| 61 6c 73 6f 20 62 65 0a | 25 25 20 75 73 65 64 20 |also be.|%% used |
|00000740| 65 69 74 68 65 72 20 69 | 6e 20 70 6c 61 63 65 20 |either i|n place |
|00000750| 6f 66 20 5c 74 68 69 63 | 6b 6e 65 73 73 20 6f 72 |of \thic|kness or|
|00000760| 20 67 6c 6f 62 61 6c 6c | 79 3b 20 74 68 65 20 64 | globall|y; the d|
|00000770| 65 66 61 75 6c 74 20 69 | 73 20 30 2e 30 34 65 6d |efault i|s 0.04em|
|00000780| 2e 0a 25 25 20 5c 70 72 | 6f 6f 66 64 6f 74 73 65 |..%% \pr|oofdotse|
|00000790| 70 61 72 61 74 69 6f 6e | 20 61 6e 64 20 5c 70 72 |paration| and \pr|
|000007a0| 6f 6f 66 64 6f 74 6e 75 | 6d 62 65 72 20 63 6f 6e |oofdotnu|mber con|
|000007b0| 74 72 6f 6c 20 74 68 65 | 20 73 69 7a 65 20 6f 66 |trol the| size of|
|000007c0| 20 74 68 65 0a 25 25 20 | 73 74 72 69 6e 67 20 6f | the.%% |string o|
|000007d0| 66 20 64 6f 74 73 0a 25 | 25 0a 25 25 20 49 66 20 |f dots.%|%.%% If |
|000007e0| 70 72 6f 6f 66 20 74 72 | 65 65 73 20 61 6e 64 20 |proof tr|ees and |
|000007f0| 66 6f 72 6d 75 6c 61 65 | 20 61 72 65 20 6d 69 78 |formulae| are mix|
|00000800| 65 64 2c 20 73 6f 6d 65 | 20 65 78 70 6c 69 63 69 |ed, some| explici|
|00000810| 74 20 73 70 61 63 69 6e | 67 20 69 73 20 6e 65 65 |t spacin|g is nee|
|00000820| 64 65 64 2c 0a 25 25 20 | 62 75 74 20 64 6f 6e 27 |ded,.%% |but don'|
|00000830| 74 20 70 75 74 20 61 6e | 79 74 68 69 6e 67 20 74 |t put an|ything t|
|00000840| 6f 20 74 68 65 20 6c 65 | 66 74 20 6f 66 20 74 68 |o the le|ft of th|
|00000850| 65 20 6c 65 66 74 2d 6d | 6f 73 74 20 28 6f 72 20 |e left-m|ost (or |
|00000860| 74 68 65 20 72 69 67 68 | 74 20 6f 66 0a 25 25 20 |the righ|t of.%% |
|00000870| 74 68 65 20 72 69 67 68 | 74 2d 6d 6f 73 74 29 20 |the righ|t-most) |
|00000880| 68 79 70 6f 74 68 65 73 | 69 73 2c 20 6f 72 20 70 |hypothes|is, or p|
|00000890| 75 74 20 69 74 20 69 6e | 20 62 72 61 63 65 73 2c |ut it in| braces,|
|000008a0| 20 62 65 63 61 75 73 65 | 20 74 68 69 73 20 77 69 | because| this wi|
|000008b0| 6c 6c 20 63 61 75 73 65 | 0a 25 25 20 74 68 65 20 |ll cause|.%% the |
|000008c0| 69 6e 64 65 6e 74 61 74 | 69 6f 6e 20 74 6f 20 62 |indentat|ion to b|
|000008d0| 65 20 6c 6f 73 74 2e 0a | 25 25 0a 25 25 20 42 79 |e lost..|%%.%% By|
|000008e0| 20 64 65 66 61 75 6c 74 | 20 74 68 65 20 63 6f 6e | default| the con|
|000008f0| 63 6c 75 73 69 6f 6e 20 | 69 73 20 63 65 6e 74 65 |clusion |is cente|
|00000900| 72 65 64 20 77 72 74 20 | 74 68 65 20 6c 65 66 74 |red wrt |the left|
|00000910| 2d 6d 6f 73 74 20 61 6e | 64 20 72 69 67 68 74 2d |-most an|d right-|
|00000920| 6d 6f 73 74 0a 25 25 20 | 69 6d 6d 65 64 69 61 74 |most.%% |immediat|
|00000930| 65 20 68 79 70 6f 74 68 | 65 73 65 73 20 28 6e 6f |e hypoth|eses (no|
|00000940| 74 20 74 68 65 69 72 20 | 70 72 6f 6f 66 73 29 3b |t their |proofs);|
|00000950| 20 5c 73 68 69 66 74 72 | 69 67 68 74 20 6f 72 20 | \shiftr|ight or |
|00000960| 5c 73 68 69 66 74 6c 65 | 66 74 20 6d 6f 76 65 73 |\shiftle|ft moves|
|00000970| 0a 25 25 20 69 74 20 72 | 65 6c 61 74 69 76 65 20 |.%% it r|elative |
|00000980| 74 6f 20 74 68 69 73 20 | 70 6f 73 69 74 69 6f 6e |to this |position|
|00000990| 2e 20 28 4e 6f 74 20 73 | 75 72 65 20 61 62 6f 75 |. (Not s|ure abou|
|000009a0| 74 20 74 68 69 73 20 73 | 70 65 63 69 66 69 63 61 |t this s|pecifica|
|000009b0| 74 69 6f 6e 20 6f 72 20 | 68 6f 77 0a 25 25 20 69 |tion or |how.%% i|
|000009c0| 74 20 73 68 6f 75 6c 64 | 20 61 66 66 65 63 74 20 |t should| affect |
|000009d0| 73 70 72 65 61 64 69 6e | 67 20 6f 66 20 70 72 6f |spreadin|g of pro|
|000009e0| 6f 66 20 74 72 65 65 2e | 29 0a 25 0a 25 20 67 6c |of tree.|).%.% gl|
|000009f0| 6f 62 61 6c 20 61 73 73 | 69 67 6e 6d 65 6e 74 73 |obal ass|ignments|
|00000a00| 20 74 6f 20 64 69 6d 65 | 6e 73 69 6f 6e 73 20 73 | to dime|nsions s|
|00000a10| 65 65 6d 20 74 6f 20 68 | 61 76 65 20 74 68 65 20 |eem to h|ave the |
|00000a20| 65 66 66 65 63 74 20 6f | 66 20 73 74 72 65 74 63 |effect o|f stretc|
|00000a30| 68 69 6e 67 0a 25 20 64 | 69 61 67 72 61 6d 73 20 |hing.% d|iagrams |
|00000a40| 68 6f 72 69 7a 6f 6e 74 | 61 6c 6c 79 2e 0a 25 0a |horizont|ally..%.|
|00000a50| 25 25 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |%%======|========|
|00000a60| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000a70| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000a80| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000a90| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 0a 0a 5c 64 |========|====..\d|
|00000aa0| 65 66 5c 69 6e 74 72 6f | 72 75 6c 65 7b 7b 5c 63 |ef\intro|rule{{\c|
|00000ab0| 61 6c 20 49 7d 7d 5c 64 | 65 66 5c 65 6c 69 6d 72 |al I}}\d|ef\elimr|
|00000ac0| 75 6c 65 7b 7b 5c 63 61 | 6c 20 45 7d 7d 25 25 0a |ule{{\ca|l E}}%%.|
|00000ad0| 5c 64 65 66 5c 61 6e 64 | 69 6e 74 72 6f 7b 5c 75 |\def\and|intro{\u|
|00000ae0| 73 69 6e 67 7b 5c 6c 61 | 6e 64 7d 5c 69 6e 74 72 |sing{\la|nd}\intr|
|00000af0| 6f 72 75 6c 65 5c 6a 75 | 73 74 69 66 69 65 73 7d |orule\ju|stifies}|
|00000b00| 25 25 0a 5c 64 65 66 5c | 69 6d 70 65 6c 69 6d 7b |%%.\def\|impelim{|
|00000b10| 5c 75 73 69 6e 67 7b 5c | 52 69 67 68 74 61 72 72 |\using{\|Rightarr|
|00000b20| 6f 77 7d 5c 65 6c 69 6d | 72 75 6c 65 5c 6a 75 73 |ow}\elim|rule\jus|
|00000b30| 74 69 66 69 65 73 7d 25 | 25 0a 5c 64 65 66 5c 61 |tifies}%|%.\def\a|
|00000b40| 6c 6c 69 6e 74 72 6f 7b | 5c 75 73 69 6e 67 7b 5c |llintro{|\using{\|
|00000b50| 66 6f 72 61 6c 6c 7d 5c | 69 6e 74 72 6f 72 75 6c |forall}\|introrul|
|00000b60| 65 5c 6a 75 73 74 69 66 | 69 65 73 7d 25 25 0a 5c |e\justif|ies}%%.\|
|00000b70| 64 65 66 5c 61 6c 6c 65 | 6c 69 6d 7b 5c 75 73 69 |def\alle|lim{\usi|
|00000b80| 6e 67 7b 5c 66 6f 72 61 | 6c 6c 7d 5c 65 6c 69 6d |ng{\fora|ll}\elim|
|00000b90| 72 75 6c 65 5c 6a 75 73 | 74 69 66 69 65 73 7d 25 |rule\jus|tifies}%|
|00000ba0| 25 0a 5c 64 65 66 5c 66 | 61 6c 73 65 65 6c 69 6d |%.\def\f|alseelim|
|00000bb0| 7b 5c 75 73 69 6e 67 7b | 5c 62 6f 74 7d 5c 65 6c |{\using{|\bot}\el|
|00000bc0| 69 6d 72 75 6c 65 5c 6a | 75 73 74 69 66 69 65 73 |imrule\j|ustifies|
|00000bd0| 7d 25 25 0a 5c 64 65 66 | 5c 65 78 69 73 74 73 69 |}%%.\def|\existsi|
|00000be0| 6e 74 72 6f 7b 5c 75 73 | 69 6e 67 7b 5c 65 78 69 |ntro{\us|ing{\exi|
|00000bf0| 73 74 73 7d 5c 69 6e 74 | 72 6f 72 75 6c 65 5c 6a |sts}\int|rorule\j|
|00000c00| 75 73 74 69 66 69 65 73 | 7d 25 25 0a 0a 25 25 20 |ustifies|}%%..%% |
|00000c10| 23 31 20 69 73 20 6d 65 | 61 6e 74 20 74 6f 20 62 |#1 is me|ant to b|
|00000c20| 65 20 31 20 6f 72 20 32 | 20 66 6f 72 20 74 68 65 |e 1 or 2| for the|
|00000c30| 20 66 69 72 73 74 20 6f | 72 20 73 65 63 6f 6e 64 | first o|r second|
|00000c40| 20 66 6f 72 6d 75 6c 61 | 0a 5c 64 65 66 5c 61 6e | formula|.\def\an|
|00000c50| 64 65 6c 69 6d 23 31 7b | 5c 75 73 69 6e 67 7b 5c |delim#1{|\using{\|
|00000c60| 6c 61 6e 64 7d 23 31 5c | 65 6c 69 6d 72 75 6c 65 |land}#1\|elimrule|
|00000c70| 5c 6a 75 73 74 69 66 69 | 65 73 7d 25 25 0a 5c 64 |\justifi|es}%%.\d|
|00000c80| 65 66 5c 6f 72 69 6e 74 | 72 6f 23 31 7b 5c 75 73 |ef\orint|ro#1{\us|
|00000c90| 69 6e 67 7b 5c 6c 6f 72 | 7d 23 31 5c 69 6e 74 72 |ing{\lor|}#1\intr|
|00000ca0| 6f 72 75 6c 65 5c 6a 75 | 73 74 69 66 69 65 73 7d |orule\ju|stifies}|
|00000cb0| 25 25 0a 0a 25 25 20 23 | 31 20 69 73 20 6d 65 61 |%%..%% #|1 is mea|
|00000cc0| 6e 74 20 74 6f 20 62 65 | 20 61 20 6c 61 62 65 6c |nt to be| a label|
|00000cd0| 20 63 6f 72 72 65 73 70 | 6f 6e 64 69 6e 67 20 74 | corresp|onding t|
|00000ce0| 6f 20 74 68 65 20 64 69 | 73 63 68 61 72 67 65 64 |o the di|scharged|
|00000cf0| 20 68 79 70 6f 74 68 65 | 73 69 73 2f 65 73 0a 5c | hypothe|sis/es.\|
|00000d00| 64 65 66 5c 69 6d 70 69 | 6e 74 72 6f 23 31 7b 5c |def\impi|ntro#1{\|
|00000d10| 75 73 69 6e 67 7b 5c 52 | 69 67 68 74 61 72 72 6f |using{\R|ightarro|
|00000d20| 77 7d 5c 69 6e 74 72 6f | 72 75 6c 65 5f 7b 23 31 |w}\intro|rule_{#1|
|00000d30| 7d 5c 6a 75 73 74 69 66 | 69 65 73 7d 25 25 0a 5c |}\justif|ies}%%.\|
|00000d40| 64 65 66 5c 6f 72 65 6c | 69 6d 23 31 7b 5c 75 73 |def\orel|im#1{\us|
|00000d50| 69 6e 67 7b 5c 6c 6f 72 | 7d 5c 65 6c 69 6d 72 75 |ing{\lor|}\elimru|
|00000d60| 6c 65 5f 7b 23 31 7d 5c | 6a 75 73 74 69 66 69 65 |le_{#1}\|justifie|
|00000d70| 73 7d 25 25 0a 5c 64 65 | 66 5c 65 78 69 73 74 73 |s}%%.\de|f\exists|
|00000d80| 65 6c 69 6d 23 31 7b 5c | 75 73 69 6e 67 7b 5c 65 |elim#1{\|using{\e|
|00000d90| 78 69 73 74 73 7d 5c 65 | 6c 69 6d 72 75 6c 65 5f |xists}\e|limrule_|
|00000da0| 7b 23 31 7d 5c 6a 75 73 | 74 69 66 69 65 73 7d 0a |{#1}\jus|tifies}.|
|00000db0| 0a 25 25 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |.%%=====|========|
|00000dc0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000dd0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000de0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00000df0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 0a 0a 5c |========|=====..\|
|00000e00| 6e 65 77 64 69 6d 65 6e | 5c 70 72 6f 6f 66 72 75 |newdimen|\proofru|
|00000e10| 6c 65 62 72 65 61 64 74 | 68 20 5c 70 72 6f 6f 66 |lebreadt|h \proof|
|00000e20| 72 75 6c 65 62 72 65 61 | 64 74 68 3d 2e 30 35 65 |rulebrea|dth=.05e|
|00000e30| 6d 0a 5c 6e 65 77 64 69 | 6d 65 6e 5c 70 72 6f 6f |m.\newdi|men\proo|
|00000e40| 66 64 6f 74 73 65 70 61 | 72 61 74 69 6f 6e 20 5c |fdotsepa|ration \|
|00000e50| 70 72 6f 6f 66 64 6f 74 | 73 65 70 61 72 61 74 69 |proofdot|separati|
|00000e60| 6f 6e 3d 31 2e 32 35 65 | 78 0a 5c 6e 65 77 64 69 |on=1.25e|x.\newdi|
|00000e70| 6d 65 6e 5c 70 72 6f 6f | 66 72 75 6c 65 62 61 73 |men\proo|frulebas|
|00000e80| 65 6c 69 6e 65 20 5c 70 | 72 6f 6f 66 72 75 6c 65 |eline \p|roofrule|
|00000e90| 62 61 73 65 6c 69 6e 65 | 3d 32 65 78 0a 5c 6e 65 |baseline|=2ex.\ne|
|00000ea0| 77 63 6f 75 6e 74 5c 70 | 72 6f 6f 66 64 6f 74 6e |wcount\p|roofdotn|
|00000eb0| 75 6d 62 65 72 20 5c 70 | 72 6f 6f 66 64 6f 74 6e |umber \p|roofdotn|
|00000ec0| 75 6d 62 65 72 3d 33 0a | 5c 6c 65 74 5c 74 68 65 |umber=3.|\let\the|
|00000ed0| 6e 5c 72 65 6c 61 78 0a | 5c 64 65 66 5c 68 66 69 |n\relax.|\def\hfi|
|00000ee0| 7b 5c 68 73 6b 69 70 30 | 70 74 20 70 6c 75 73 2e |{\hskip0|pt plus.|
|00000ef0| 30 30 30 31 66 69 6c 7d | 0a 5c 6d 61 74 68 63 68 |0001fil}|.\mathch|
|00000f00| 61 72 64 65 66 5c 73 71 | 75 69 67 74 6f 3d 22 33 |ardef\sq|uigto="3|
|00000f10| 41 33 42 0a 25 0a 25 20 | 66 6c 61 67 20 77 68 65 |A3B.%.% |flag whe|
|00000f20| 72 65 20 77 65 20 61 72 | 65 0a 5c 6e 65 77 69 66 |re we ar|e.\newif|
|00000f30| 5c 69 66 69 6e 73 69 64 | 65 70 72 6f 6f 66 74 72 |\ifinsid|eprooftr|
|00000f40| 65 65 5c 69 6e 73 69 64 | 65 70 72 6f 6f 66 74 72 |ee\insid|eprooftr|
|00000f50| 65 65 66 61 6c 73 65 0a | 5c 6e 65 77 69 66 5c 69 |eefalse.|\newif\i|
|00000f60| 66 6f 6e 6c 65 66 74 6f | 66 70 72 6f 6f 66 72 75 |fonlefto|fproofru|
|00000f70| 6c 65 5c 6f 6e 6c 65 66 | 74 6f 66 70 72 6f 6f 66 |le\onlef|tofproof|
|00000f80| 72 75 6c 65 66 61 6c 73 | 65 0a 5c 6e 65 77 69 66 |rulefals|e.\newif|
|00000f90| 5c 69 66 70 72 6f 6f 66 | 64 6f 74 73 5c 70 72 6f |\ifproof|dots\pro|
|00000fa0| 6f 66 64 6f 74 73 66 61 | 6c 73 65 0a 5c 6e 65 77 |ofdotsfa|lse.\new|
|00000fb0| 69 66 5c 69 66 64 6f 75 | 62 6c 65 70 72 6f 6f 66 |if\ifdou|bleproof|
|00000fc0| 5c 64 6f 75 62 6c 65 70 | 72 6f 6f 66 66 61 6c 73 |\doublep|rooffals|
|00000fd0| 65 0a 5c 6c 65 74 5c 77 | 65 72 65 69 6e 70 72 6f |e.\let\w|ereinpro|
|00000fe0| 6f 66 62 69 74 5c 72 65 | 6c 61 78 0a 25 0a 25 20 |ofbit\re|lax.%.% |
|00000ff0| 64 69 6d 65 6e 73 69 6f | 6e 73 20 61 6e 64 20 62 |dimensio|ns and b|
|00001000| 6f 78 65 73 20 6f 66 20 | 62 69 74 73 0a 5c 6e 65 |oxes of |bits.\ne|
|00001010| 77 64 69 6d 65 6e 5c 73 | 68 6f 72 74 65 6e 70 72 |wdimen\s|hortenpr|
|00001020| 6f 6f 66 6c 65 66 74 0a | 5c 6e 65 77 64 69 6d 65 |oofleft.|\newdime|
|00001030| 6e 5c 73 68 6f 72 74 65 | 6e 70 72 6f 6f 66 72 69 |n\shorte|nproofri|
|00001040| 67 68 74 0a 5c 6e 65 77 | 64 69 6d 65 6e 5c 70 72 |ght.\new|dimen\pr|
|00001050| 6f 6f 66 62 65 6c 6f 77 | 73 68 69 66 74 0a 5c 6e |oofbelow|shift.\n|
|00001060| 65 77 62 6f 78 5c 70 72 | 6f 6f 66 61 62 6f 76 65 |ewbox\pr|oofabove|
|00001070| 0a 5c 6e 65 77 62 6f 78 | 5c 70 72 6f 6f 66 62 65 |.\newbox|\proofbe|
|00001080| 6c 6f 77 0a 5c 6e 65 77 | 62 6f 78 5c 70 72 6f 6f |low.\new|box\proo|
|00001090| 66 72 75 6c 65 6e 61 6d | 65 0a 25 0a 25 20 6d 69 |frulenam|e.%.% mi|
|000010a0| 73 63 65 6c 6c 61 6e 65 | 6f 75 73 20 63 6f 6d 6d |scellane|ous comm|
|000010b0| 61 6e 64 73 20 66 6f 72 | 20 73 65 74 74 69 6e 67 |ands for| setting|
|000010c0| 20 76 61 6c 75 65 73 0a | 5c 64 65 66 5c 73 68 69 | values.|\def\shi|
|000010d0| 66 74 70 72 6f 6f 66 62 | 65 6c 6f 77 7b 5c 6c 65 |ftproofb|elow{\le|
|000010e0| 74 5c 6e 65 78 74 5c 72 | 65 6c 61 78 5c 61 66 74 |t\next\r|elax\aft|
|000010f0| 65 72 61 73 73 69 67 6e | 6d 65 6e 74 5c 73 65 74 |erassign|ment\set|
|00001100| 73 68 69 66 74 70 72 6f | 6f 66 62 65 6c 6f 77 5c |shiftpro|ofbelow\|
|00001110| 64 69 6d 65 6e 30 20 7d | 0a 5c 64 65 66 5c 73 68 |dimen0 }|.\def\sh|
|00001120| 69 66 74 70 72 6f 6f 66 | 62 65 6c 6f 77 6e 65 67 |iftproof|belowneg|
|00001130| 7b 5c 64 65 66 5c 6e 65 | 78 74 7b 5c 6d 75 6c 74 |{\def\ne|xt{\mult|
|00001140| 69 70 6c 79 5c 64 69 6d | 65 6e 30 20 62 79 2d 31 |iply\dim|en0 by-1|
|00001150| 20 7d 25 0a 5c 61 66 74 | 65 72 61 73 73 69 67 6e | }%.\aft|erassign|
|00001160| 6d 65 6e 74 5c 73 65 74 | 73 68 69 66 74 70 72 6f |ment\set|shiftpro|
|00001170| 6f 66 62 65 6c 6f 77 5c | 64 69 6d 65 6e 30 20 7d |ofbelow\|dimen0 }|
|00001180| 0a 5c 64 65 66 5c 73 65 | 74 73 68 69 66 74 70 72 |.\def\se|tshiftpr|
|00001190| 6f 6f 66 62 65 6c 6f 77 | 7b 5c 6e 65 78 74 5c 70 |oofbelow|{\next\p|
|000011a0| 72 6f 6f 66 62 65 6c 6f | 77 73 68 69 66 74 3d 5c |roofbelo|wshift=\|
|000011b0| 64 69 6d 65 6e 30 20 7d | 0a 5c 64 65 66 5c 73 65 |dimen0 }|.\def\se|
|000011c0| 74 70 72 6f 6f 66 72 75 | 6c 65 62 72 65 61 64 74 |tproofru|lebreadt|
|000011d0| 68 7b 5c 70 72 6f 6f 66 | 72 75 6c 65 62 72 65 61 |h{\proof|rulebrea|
|000011e0| 64 74 68 7d 0a 0a 25 3d | 3d 3d 3d 3d 3d 3d 3d 3d |dth}..%=|========|
|000011f0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001200| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001210| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001220| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001230| 3d 3d 3d 3d 0a 5c 64 65 | 66 5c 70 72 6f 6f 66 74 |====.\de|f\prooft|
|00001240| 72 65 65 7b 25 20 4e 45 | 53 54 45 44 20 5a 45 52 |ree{% NE|STED ZER|
|00001250| 4f 20 28 5c 69 66 6f 6e | 6c 65 66 74 6f 66 70 72 |O (\ifon|leftofpr|
|00001260| 6f 6f 66 72 75 6c 65 29 | 0a 25 0a 25 20 66 69 72 |oofrule)|.%.% fir|
|00001270| 73 74 20 66 69 6e 64 20 | 6f 75 74 20 77 68 65 74 |st find |out whet|
|00001280| 68 65 72 20 77 65 27 72 | 65 20 61 74 20 74 68 65 |her we'r|e at the|
|00001290| 20 6c 65 66 74 2d 68 61 | 6e 64 20 65 6e 64 20 6f | left-ha|nd end o|
|000012a0| 66 20 61 20 70 72 6f 6f | 66 20 72 75 6c 65 0a 5c |f a proo|f rule.\|
|000012b0| 69 66 6e 75 6d 09 5c 6c | 61 73 74 70 65 6e 61 6c |ifnum.\l|astpenal|
|000012c0| 74 79 3d 31 0a 5c 74 68 | 65 6e 09 5c 75 6e 70 65 |ty=1.\th|en.\unpe|
|000012d0| 6e 61 6c 74 79 0a 5c 65 | 6c 73 65 09 5c 6f 6e 6c |nalty.\e|lse.\onl|
|000012e0| 65 66 74 6f 66 70 72 6f | 6f 66 72 75 6c 65 66 61 |eftofpro|ofrulefa|
|000012f0| 6c 73 65 0a 5c 66 69 0a | 25 0a 25 20 73 6f 6d 65 |lse.\fi.|%.% some|
|00001300| 20 73 70 61 63 65 20 6f | 6e 20 6c 65 66 74 20 28 | space o|n left (|
|00001310| 65 78 63 65 70 74 20 69 | 66 20 77 65 27 72 65 20 |except i|f we're |
|00001320| 6f 6e 20 6c 65 66 74 2c | 20 61 6e 64 20 6e 6f 20 |on left,| and no |
|00001330| 69 6e 66 69 6e 69 74 79 | 20 66 6f 72 20 6f 75 74 |infinity| for out|
|00001340| 65 72 6d 6f 73 74 29 0a | 5c 69 66 6f 6e 6c 65 66 |ermost).|\ifonlef|
|00001350| 74 6f 66 70 72 6f 6f 66 | 72 75 6c 65 0a 5c 65 6c |tofproof|rule.\el|
|00001360| 73 65 09 5c 69 66 69 6e | 73 69 64 65 70 72 6f 6f |se.\ifin|sideproo|
|00001370| 66 74 72 65 65 0a 09 5c | 74 68 65 6e 09 5c 68 73 |ftree..\|then.\hs|
|00001380| 6b 69 70 2e 35 65 6d 20 | 70 6c 75 73 31 66 69 6c |kip.5em |plus1fil|
|00001390| 0a 09 5c 66 69 0a 5c 66 | 69 0a 25 0a 25 20 62 65 |..\fi.\f|i.%.% be|
|000013a0| 67 69 6e 20 6f 75 72 20 | 70 72 6f 6f 66 20 74 72 |gin our |proof tr|
|000013b0| 65 65 20 65 6e 76 69 72 | 6f 6e 6d 65 6e 74 0a 5c |ee envir|onment.\|
|000013c0| 62 67 72 6f 75 70 25 20 | 4e 45 53 54 45 44 20 4f |bgroup% |NESTED O|
|000013d0| 4e 45 20 28 5c 70 72 6f | 6f 66 62 65 6c 6f 77 2c |NE (\pro|ofbelow,|
|000013e0| 20 5c 70 72 6f 6f 66 72 | 75 6c 65 6e 61 6d 65 2c | \proofr|ulename,|
|000013f0| 20 5c 70 72 6f 6f 66 61 | 62 6f 76 65 2c 0a 25 09 | \proofa|bove,.%.|
|00001400| 09 5c 73 68 6f 72 74 65 | 6e 70 72 6f 6f 66 6c 65 |.\shorte|nproofle|
|00001410| 66 74 2c 20 5c 73 68 6f | 72 74 65 6e 70 72 6f 6f |ft, \sho|rtenproo|
|00001420| 66 72 69 67 68 74 2c 20 | 5c 70 72 6f 6f 66 72 75 |fright, |\proofru|
|00001430| 6c 65 62 72 65 61 64 74 | 68 29 0a 5c 73 65 74 62 |lebreadt|h).\setb|
|00001440| 6f 78 5c 70 72 6f 6f 66 | 62 65 6c 6f 77 3d 5c 68 |ox\proof|below=\h|
|00001450| 62 6f 78 7b 7d 5c 73 65 | 74 62 6f 78 5c 70 72 6f |box{}\se|tbox\pro|
|00001460| 6f 66 72 75 6c 65 6e 61 | 6d 65 3d 5c 68 62 6f 78 |ofrulena|me=\hbox|
|00001470| 7b 7d 25 0a 5c 6c 65 74 | 5c 6a 75 73 74 69 66 69 |{}%.\let|\justifi|
|00001480| 65 73 5c 70 72 6f 6f 66 | 6f 76 65 72 5c 6c 65 74 |es\proof|over\let|
|00001490| 5c 6c 65 61 64 73 74 6f | 5c 70 72 6f 6f 66 6f 76 |\leadsto|\proofov|
|000014a0| 65 72 64 6f 74 73 5c 6c | 65 74 5c 4a 75 73 74 69 |erdots\l|et\Justi|
|000014b0| 66 69 65 73 5c 70 72 6f | 6f 66 6f 76 65 72 64 62 |fies\pro|ofoverdb|
|000014c0| 6c 0a 5c 6c 65 74 5c 75 | 73 69 6e 67 5c 70 72 6f |l.\let\u|sing\pro|
|000014d0| 6f 66 75 73 69 6e 67 5c | 6c 65 74 5c 5b 5c 70 72 |ofusing\|let\[\pr|
|000014e0| 6f 6f 66 74 72 65 65 0a | 5c 69 66 69 6e 73 69 64 |ooftree.|\ifinsid|
|000014f0| 65 70 72 6f 6f 66 74 72 | 65 65 5c 6c 65 74 5c 5d |eprooftr|ee\let\]|
|00001500| 5c 65 6e 64 70 72 6f 6f | 66 74 72 65 65 5c 66 69 |\endproo|ftree\fi|
|00001510| 0a 5c 70 72 6f 6f 66 64 | 6f 74 73 66 61 6c 73 65 |.\proofd|otsfalse|
|00001520| 5c 64 6f 75 62 6c 65 70 | 72 6f 6f 66 66 61 6c 73 |\doublep|rooffals|
|00001530| 65 0a 5c 6c 65 74 5c 74 | 68 69 63 6b 6e 65 73 73 |e.\let\t|hickness|
|00001540| 5c 73 65 74 70 72 6f 6f | 66 72 75 6c 65 62 72 65 |\setproo|frulebre|
|00001550| 61 64 74 68 0a 5c 6c 65 | 74 5c 73 68 69 66 74 72 |adth.\le|t\shiftr|
|00001560| 69 67 68 74 5c 73 68 69 | 66 74 70 72 6f 6f 66 62 |ight\shi|ftproofb|
|00001570| 65 6c 6f 77 20 5c 6c 65 | 74 5c 73 68 69 66 74 5c |elow \le|t\shift\|
|00001580| 73 68 69 66 74 70 72 6f | 6f 66 62 65 6c 6f 77 0a |shiftpro|ofbelow.|
|00001590| 5c 6c 65 74 5c 73 68 69 | 66 74 6c 65 66 74 5c 73 |\let\shi|ftleft\s|
|000015a0| 68 69 66 74 70 72 6f 6f | 66 62 65 6c 6f 77 6e 65 |hiftproo|fbelowne|
|000015b0| 67 0a 5c 6c 65 74 5c 69 | 66 77 61 73 69 6e 73 69 |g.\let\i|fwasinsi|
|000015c0| 64 65 70 72 6f 6f 66 74 | 72 65 65 5c 69 66 69 6e |deprooft|ree\ifin|
|000015d0| 73 69 64 65 70 72 6f 6f | 66 74 72 65 65 0a 5c 69 |sideproo|ftree.\i|
|000015e0| 6e 73 69 64 65 70 72 6f | 6f 66 74 72 65 65 74 72 |nsidepro|oftreetr|
|000015f0| 75 65 0a 25 0a 25 20 6e | 6f 77 20 62 65 67 69 6e |ue.%.% n|ow begin|
|00001600| 20 74 6f 20 73 65 74 20 | 74 68 65 20 74 6f 70 20 | to set |the top |
|00001610| 6f 66 20 74 68 65 20 72 | 75 6c 65 20 28 64 65 66 |of the r|ule (def|
|00001620| 69 6e 69 74 69 6f 6e 73 | 20 6c 6f 63 61 6c 20 74 |initions| local t|
|00001630| 6f 20 69 74 29 0a 5c 73 | 65 74 62 6f 78 5c 70 72 |o it).\s|etbox\pr|
|00001640| 6f 6f 66 61 62 6f 76 65 | 3d 5c 68 62 6f 78 5c 62 |oofabove|=\hbox\b|
|00001650| 67 72 6f 75 70 24 5c 64 | 69 73 70 6c 61 79 73 74 |group$\d|isplayst|
|00001660| 79 6c 65 20 25 20 4e 45 | 53 54 45 44 20 54 57 4f |yle % NE|STED TWO|
|00001670| 0a 5c 6c 65 74 5c 77 65 | 72 65 69 6e 70 72 6f 6f |.\let\we|reinproo|
|00001680| 66 62 69 74 5c 70 72 6f | 6f 66 74 72 65 65 0a 25 |fbit\pro|oftree.%|
|00001690| 0a 25 20 74 68 65 73 65 | 20 6c 6f 63 61 6c 20 76 |.% these| local v|
|000016a0| 61 72 69 61 62 6c 65 73 | 20 77 69 6c 6c 20 62 65 |ariables| will be|
|000016b0| 20 63 6f 70 69 65 64 20 | 6f 75 74 3a 0a 5c 73 68 | copied |out:.\sh|
|000016c0| 6f 72 74 65 6e 70 72 6f | 6f 66 6c 65 66 74 3d 30 |ortenpro|ofleft=0|
|000016d0| 70 74 20 5c 73 68 6f 72 | 74 65 6e 70 72 6f 6f 66 |pt \shor|tenproof|
|000016e0| 72 69 67 68 74 3d 30 70 | 74 20 5c 70 72 6f 6f 66 |right=0p|t \proof|
|000016f0| 62 65 6c 6f 77 73 68 69 | 66 74 3d 30 70 74 0a 25 |belowshi|ft=0pt.%|
|00001700| 0a 25 20 66 6c 61 67 73 | 20 74 6f 20 65 6e 61 62 |.% flags| to enab|
|00001710| 6c 65 20 69 6e 6e 65 72 | 20 70 72 6f 6f 66 20 74 |le inner| proof t|
|00001720| 72 65 65 20 74 6f 20 64 | 65 74 65 63 74 20 69 66 |ree to d|etect if|
|00001730| 20 6f 6e 20 6c 65 66 74 | 3a 0a 5c 6f 6e 6c 65 66 | on left|:.\onlef|
|00001740| 74 6f 66 70 72 6f 6f 66 | 72 75 6c 65 74 72 75 65 |tofproof|ruletrue|
|00001750| 5c 70 65 6e 61 6c 74 79 | 31 0a 7d 0a 0a 25 3d 3d |\penalty|1.}..%==|
|00001760| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001770| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001780| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001790| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|000017a0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 0a 25 20 65 6e |========|===.% en|
|000017b0| 64 20 77 68 61 74 65 76 | 65 72 20 62 6f 78 20 61 |d whatev|er box a|
|000017c0| 6e 64 20 63 6f 70 79 20 | 63 72 75 63 69 61 6c 20 |nd copy |crucial |
|000017d0| 76 61 6c 75 65 73 20 6f | 75 74 20 6f 66 20 69 74 |values o|ut of it|
|000017e0| 0a 5c 64 65 66 5c 65 70 | 72 6f 6f 66 62 69 74 7b |.\def\ep|roofbit{|
|000017f0| 25 20 4e 45 53 54 45 44 | 20 54 57 4f 0a 25 0a 25 |% NESTED| TWO.%.%|
|00001800| 20 76 61 72 69 6f 75 73 | 20 68 61 63 6b 73 20 61 | various| hacks a|
|00001810| 70 70 6c 69 63 61 62 6c | 65 20 74 6f 20 68 79 70 |pplicabl|e to hyp|
|00001820| 6f 74 68 65 73 69 73 20 | 6c 69 73 74 20 0a 5c 69 |othesis |list .\i|
|00001830| 66 78 09 5c 77 65 72 65 | 69 6e 70 72 6f 6f 66 62 |fx.\were|inproofb|
|00001840| 69 74 5c 70 72 6f 6f 66 | 74 72 65 65 0a 5c 74 68 |it\proof|tree.\th|
|00001850| 65 6e 09 5c 69 66 63 61 | 73 65 09 5c 6c 61 73 74 |en.\ifca|se.\last|
|00001860| 70 65 6e 61 6c 74 79 0a | 09 5c 74 68 65 6e 09 5c |penalty.|.\then.\|
|00001870| 73 68 6f 72 74 65 6e 70 | 72 6f 6f 66 72 69 67 68 |shortenp|roofrigh|
|00001880| 74 3d 30 70 74 09 25 20 | 30 3a 20 73 6f 6d 65 20 |t=0pt.% |0: some |
|00001890| 6f 74 68 65 72 20 6f 62 | 6a 65 63 74 2c 20 6e 6f |other ob|ject, no|
|000018a0| 20 69 6e 64 65 6e 74 61 | 74 69 6f 6e 0a 09 5c 6f | indenta|tion..\o|
|000018b0| 72 09 5c 75 6e 70 65 6e | 61 6c 74 79 5c 68 66 69 |r.\unpen|alty\hfi|
|000018c0| 6c 09 09 25 20 31 3a 20 | 65 6d 70 74 79 20 68 79 |l..% 1: |empty hy|
|000018d0| 70 6f 74 68 65 73 65 73 | 2c 20 6a 75 73 74 20 67 |potheses|, just g|
|000018e0| 6c 75 65 0a 09 5c 6f 72 | 09 5c 75 6e 70 65 6e 61 |lue..\or|.\unpena|
|000018f0| 6c 74 79 5c 75 6e 73 6b | 69 70 09 25 20 32 3a 20 |lty\unsk|ip.% 2: |
|00001900| 6a 75 73 74 20 68 61 64 | 20 61 20 74 72 65 65 2c |just had| a tree,|
|00001910| 20 72 65 6d 6f 76 65 20 | 67 6c 75 65 0a 09 5c 65 | remove |glue..\e|
|00001920| 6c 73 65 09 5c 73 68 6f | 72 74 65 6e 70 72 6f 6f |lse.\sho|rtenproo|
|00001930| 66 72 69 67 68 74 3d 30 | 70 74 09 25 20 65 68 3f |fright=0|pt.% eh?|
|00001940| 0a 09 5c 66 69 0a 5c 66 | 69 0a 25 0a 25 20 70 61 |..\fi.\f|i.%.% pa|
|00001950| 73 73 20 6f 75 74 20 63 | 72 75 63 69 61 6c 20 76 |ss out c|rucial v|
|00001960| 61 6c 75 65 73 20 66 72 | 6f 6d 20 73 63 6f 70 65 |alues fr|om scope|
|00001970| 0a 5c 67 6c 6f 62 61 6c | 5c 64 69 6d 65 6e 30 3d |.\global|\dimen0=|
|00001980| 5c 73 68 6f 72 74 65 6e | 70 72 6f 6f 66 6c 65 66 |\shorten|prooflef|
|00001990| 74 0a 5c 67 6c 6f 62 61 | 6c 5c 64 69 6d 65 6e 31 |t.\globa|l\dimen1|
|000019a0| 3d 5c 73 68 6f 72 74 65 | 6e 70 72 6f 6f 66 72 69 |=\shorte|nproofri|
|000019b0| 67 68 74 0a 5c 67 6c 6f | 62 61 6c 5c 64 69 6d 65 |ght.\glo|bal\dime|
|000019c0| 6e 32 3d 5c 70 72 6f 6f | 66 72 75 6c 65 62 72 65 |n2=\proo|frulebre|
|000019d0| 61 64 74 68 0a 5c 67 6c | 6f 62 61 6c 5c 64 69 6d |adth.\gl|obal\dim|
|000019e0| 65 6e 33 3d 5c 70 72 6f | 6f 66 62 65 6c 6f 77 73 |en3=\pro|ofbelows|
|000019f0| 68 69 66 74 0a 5c 67 6c | 6f 62 61 6c 5c 64 69 6d |hift.\gl|obal\dim|
|00001a00| 65 6e 34 3d 5c 70 72 6f | 6f 66 64 6f 74 73 65 70 |en4=\pro|ofdotsep|
|00001a10| 61 72 61 74 69 6f 6e 0a | 5c 67 6c 6f 62 61 6c 5c |aration.|\global\|
|00001a20| 6d 73 63 6f 75 6e 74 3d | 5c 70 72 6f 6f 66 64 6f |mscount=|\proofdo|
|00001a30| 74 6e 75 6d 62 65 72 0a | 25 0a 25 20 65 6e 64 20 |tnumber.|%.% end |
|00001a40| 74 68 65 20 62 6f 78 0a | 24 5c 65 67 72 6f 75 70 |the box.|$\egroup|
|00001a50| 20 20 25 20 4e 45 53 54 | 45 44 20 4f 4e 45 0a 25 | % NEST|ED ONE.%|
|00001a60| 0a 25 20 72 65 73 74 6f | 72 65 20 74 68 65 20 76 |.% resto|re the v|
|00001a70| 61 6c 75 65 73 0a 5c 73 | 68 6f 72 74 65 6e 70 72 |alues.\s|hortenpr|
|00001a80| 6f 6f 66 6c 65 66 74 3d | 5c 64 69 6d 65 6e 30 0a |oofleft=|\dimen0.|
|00001a90| 5c 73 68 6f 72 74 65 6e | 70 72 6f 6f 66 72 69 67 |\shorten|proofrig|
|00001aa0| 68 74 3d 5c 64 69 6d 65 | 6e 31 0a 5c 70 72 6f 6f |ht=\dime|n1.\proo|
|00001ab0| 66 72 75 6c 65 62 72 65 | 61 64 74 68 3d 5c 64 69 |frulebre|adth=\di|
|00001ac0| 6d 65 6e 32 0a 5c 70 72 | 6f 6f 66 62 65 6c 6f 77 |men2.\pr|oofbelow|
|00001ad0| 73 68 69 66 74 3d 5c 64 | 69 6d 65 6e 33 0a 5c 70 |shift=\d|imen3.\p|
|00001ae0| 72 6f 6f 66 64 6f 74 73 | 65 70 61 72 61 74 69 6f |roofdots|eparatio|
|00001af0| 6e 3d 5c 64 69 6d 65 6e | 34 0a 5c 70 72 6f 6f 66 |n=\dimen|4.\proof|
|00001b00| 64 6f 74 6e 75 6d 62 65 | 72 3d 5c 6d 73 63 6f 75 |dotnumbe|r=\mscou|
|00001b10| 6e 74 0a 7d 0a 0a 25 3d | 3d 3d 3d 3d 3d 3d 3d 3d |nt.}..%=|========|
|00001b20| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001b30| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001b40| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001b50| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001b60| 3d 3d 3d 3d 0a 5c 64 65 | 66 5c 70 72 6f 6f 66 6f |====.\de|f\proofo|
|00001b70| 76 65 72 7b 25 20 4e 45 | 53 54 45 44 20 54 57 4f |ver{% NE|STED TWO|
|00001b80| 0a 5c 65 70 72 6f 6f 66 | 62 69 74 20 25 20 4e 45 |.\eproof|bit % NE|
|00001b90| 53 54 45 44 20 4f 4e 45 | 0a 5c 73 65 74 62 6f 78 |STED ONE|.\setbox|
|00001ba0| 5c 70 72 6f 6f 66 62 65 | 6c 6f 77 3d 5c 68 62 6f |\proofbe|low=\hbo|
|00001bb0| 78 5c 62 67 72 6f 75 70 | 20 25 20 4e 45 53 54 45 |x\bgroup| % NESTE|
|00001bc0| 44 20 54 57 4f 0a 5c 6c | 65 74 5c 77 65 72 65 69 |D TWO.\l|et\werei|
|00001bd0| 6e 70 72 6f 6f 66 62 69 | 74 5c 70 72 6f 6f 66 6f |nproofbi|t\proofo|
|00001be0| 76 65 72 0a 24 5c 64 69 | 73 70 6c 61 79 73 74 79 |ver.$\di|splaysty|
|00001bf0| 6c 65 0a 7d 25 0a 25 0a | 25 3d 3d 3d 3d 3d 3d 3d |le.}%.%.|%=======|
|00001c00| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001c10| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001c20| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001c30| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001c40| 3d 3d 3d 3d 3d 3d 0a 5c | 64 65 66 5c 70 72 6f 6f |======.\|def\proo|
|00001c50| 66 6f 76 65 72 64 62 6c | 7b 25 20 4e 45 53 54 45 |foverdbl|{% NESTE|
|00001c60| 44 20 54 57 4f 0a 5c 65 | 70 72 6f 6f 66 62 69 74 |D TWO.\e|proofbit|
|00001c70| 20 25 20 4e 45 53 54 45 | 44 20 4f 4e 45 0a 5c 64 | % NESTE|D ONE.\d|
|00001c80| 6f 75 62 6c 65 70 72 6f | 6f 66 74 72 75 65 0a 5c |oublepro|oftrue.\|
|00001c90| 73 65 74 62 6f 78 5c 70 | 72 6f 6f 66 62 65 6c 6f |setbox\p|roofbelo|
|00001ca0| 77 3d 5c 68 62 6f 78 5c | 62 67 72 6f 75 70 20 25 |w=\hbox\|bgroup %|
|00001cb0| 20 4e 45 53 54 45 44 20 | 54 57 4f 0a 5c 6c 65 74 | NESTED |TWO.\let|
|00001cc0| 5c 77 65 72 65 69 6e 70 | 72 6f 6f 66 62 69 74 5c |\wereinp|roofbit\|
|00001cd0| 70 72 6f 6f 66 6f 76 65 | 72 64 62 6c 0a 24 5c 64 |proofove|rdbl.$\d|
|00001ce0| 69 73 70 6c 61 79 73 74 | 79 6c 65 0a 7d 25 0a 25 |isplayst|yle.}%.%|
|00001cf0| 0a 25 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |.%======|========|
|00001d00| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001d10| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001d20| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001d30| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 0a |========|=======.|
|00001d40| 5c 64 65 66 5c 70 72 6f | 6f 66 6f 76 65 72 64 6f |\def\pro|ofoverdo|
|00001d50| 74 73 7b 25 20 4e 45 53 | 54 45 44 20 54 57 4f 0a |ts{% NES|TED TWO.|
|00001d60| 5c 65 70 72 6f 6f 66 62 | 69 74 20 25 20 4e 45 53 |\eproofb|it % NES|
|00001d70| 54 45 44 20 4f 4e 45 0a | 5c 70 72 6f 6f 66 64 6f |TED ONE.|\proofdo|
|00001d80| 74 73 74 72 75 65 0a 5c | 73 65 74 62 6f 78 5c 70 |tstrue.\|setbox\p|
|00001d90| 72 6f 6f 66 62 65 6c 6f | 77 3d 5c 68 62 6f 78 5c |roofbelo|w=\hbox\|
|00001da0| 62 67 72 6f 75 70 20 25 | 20 4e 45 53 54 45 44 20 |bgroup %| NESTED |
|00001db0| 54 57 4f 0a 5c 6c 65 74 | 5c 77 65 72 65 69 6e 70 |TWO.\let|\wereinp|
|00001dc0| 72 6f 6f 66 62 69 74 5c | 70 72 6f 6f 66 6f 76 65 |roofbit\|proofove|
|00001dd0| 72 64 6f 74 73 0a 24 5c | 64 69 73 70 6c 61 79 73 |rdots.$\|displays|
|00001de0| 74 79 6c 65 0a 7d 25 0a | 25 0a 25 3d 3d 3d 3d 3d |tyle.}%.|%.%=====|
|00001df0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001e00| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001e10| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001e20| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001e30| 3d 3d 3d 3d 3d 3d 3d 3d | 0a 5c 64 65 66 5c 70 72 |========|.\def\pr|
|00001e40| 6f 6f 66 75 73 69 6e 67 | 7b 25 20 4e 45 53 54 45 |oofusing|{% NESTE|
|00001e50| 44 20 54 57 4f 0a 5c 65 | 70 72 6f 6f 66 62 69 74 |D TWO.\e|proofbit|
|00001e60| 20 25 20 4e 45 53 54 45 | 44 20 4f 4e 45 0a 5c 73 | % NESTE|D ONE.\s|
|00001e70| 65 74 62 6f 78 5c 70 72 | 6f 6f 66 72 75 6c 65 6e |etbox\pr|oofrulen|
|00001e80| 61 6d 65 3d 5c 68 62 6f | 78 5c 62 67 72 6f 75 70 |ame=\hbo|x\bgroup|
|00001e90| 20 25 20 4e 45 53 54 45 | 44 20 54 57 4f 0a 5c 6c | % NESTE|D TWO.\l|
|00001ea0| 65 74 5c 77 65 72 65 69 | 6e 70 72 6f 6f 66 62 69 |et\werei|nproofbi|
|00001eb0| 74 5c 70 72 6f 6f 66 75 | 73 69 6e 67 0a 5c 6b 65 |t\proofu|sing.\ke|
|00001ec0| 72 6e 30 2e 33 65 6d 24 | 0a 7d 0a 0a 25 3d 3d 3d |rn0.3em$|.}..%===|
|00001ed0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001ee0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001ef0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001f00| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00001f10| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 0a 5c 64 65 66 5c |========|==.\def\|
|00001f20| 65 6e 64 70 72 6f 6f 66 | 74 72 65 65 7b 25 20 4e |endproof|tree{% N|
|00001f30| 45 53 54 45 44 20 54 57 | 4f 0a 5c 65 70 72 6f 6f |ESTED TW|O.\eproo|
|00001f40| 66 62 69 74 20 25 20 4e | 45 53 54 45 44 20 4f 4e |fbit % N|ESTED ON|
|00001f50| 45 0a 25 20 5c 64 69 6d | 65 6e 30 20 3d 09 6c 65 |E.% \dim|en0 =.le|
|00001f60| 6e 67 74 68 20 6f 66 20 | 70 72 6f 6f 66 20 72 75 |ngth of |proof ru|
|00001f70| 6c 65 0a 25 20 5c 64 69 | 6d 65 6e 31 20 3d 09 69 |le.% \di|men1 =.i|
|00001f80| 6e 64 65 6e 74 61 74 69 | 6f 6e 20 6f 66 20 63 6f |ndentati|on of co|
|00001f90| 6e 63 6c 75 73 69 6f 6e | 20 77 72 74 20 72 75 6c |nclusion| wrt rul|
|00001fa0| 65 0a 25 20 5c 64 69 6d | 65 6e 32 20 3d 09 6e 65 |e.% \dim|en2 =.ne|
|00001fb0| 77 20 5c 73 68 6f 72 74 | 65 6e 70 72 6f 6f 66 6c |w \short|enproofl|
|00001fc0| 65 66 74 2c 20 69 65 20 | 69 6e 64 65 6e 74 61 74 |eft, ie |indentat|
|00001fd0| 69 6f 6e 20 6f 66 20 63 | 6f 6e 63 6c 75 73 69 6f |ion of c|onclusio|
|00001fe0| 6e 0a 25 20 5c 64 69 6d | 65 6e 33 20 3d 09 6e 65 |n.% \dim|en3 =.ne|
|00001ff0| 77 20 5c 73 68 6f 72 74 | 65 6e 70 72 6f 6f 66 72 |w \short|enproofr|
|00002000| 69 67 68 74 2c 20 69 65 | 0a 25 09 09 20 73 70 61 |ight, ie|.%.. spa|
|00002010| 63 65 20 6f 6e 20 72 69 | 67 68 74 20 6f 66 20 63 |ce on ri|ght of c|
|00002020| 6f 6e 63 6c 75 73 69 6f | 6e 20 74 6f 20 65 6e 64 |onclusio|n to end|
|00002030| 20 6f 66 20 74 72 65 65 | 0a 25 20 5c 64 69 6d 65 | of tree|.% \dime|
|00002040| 6e 34 20 3d 09 73 70 61 | 63 65 20 6f 6e 20 72 69 |n4 =.spa|ce on ri|
|00002050| 67 68 74 20 6f 66 20 63 | 6f 6e 63 6c 75 73 69 6f |ght of c|onclusio|
|00002060| 6e 20 62 65 6c 6f 77 20 | 72 75 6c 65 0a 20 20 5c |n below |rule. \|
|00002070| 64 69 6d 65 6e 35 20 3d | 30 70 74 25 20 73 70 72 |dimen5 =|0pt% spr|
|00002080| 65 61 64 20 6f 66 20 68 | 79 70 6f 74 68 65 73 65 |ead of h|ypothese|
|00002090| 73 0a 25 20 5c 64 69 6d | 65 6e 36 2c 20 5c 64 69 |s.% \dim|en6, \di|
|000020a0| 6d 65 6e 37 20 3d 20 68 | 65 69 67 68 74 20 26 20 |men7 = h|eight & |
|000020b0| 64 65 70 74 68 20 6f 66 | 20 72 75 6c 65 0a 25 0a |depth of| rule.%.|
|000020c0| 25 20 6c 65 6e 67 74 68 | 20 6f 66 20 72 75 6c 65 |% length| of rule|
|000020d0| 20 6e 65 65 64 65 64 20 | 62 79 20 70 72 6f 6f 66 | needed |by proof|
|000020e0| 20 61 62 6f 76 65 0a 5c | 64 69 6d 65 6e 30 3d 5c | above.\|dimen0=\|
|000020f0| 77 64 5c 70 72 6f 6f 66 | 61 62 6f 76 65 20 5c 61 |wd\proof|above \a|
|00002100| 64 76 61 6e 63 65 5c 64 | 69 6d 65 6e 30 2d 5c 73 |dvance\d|imen0-\s|
|00002110| 68 6f 72 74 65 6e 70 72 | 6f 6f 66 6c 65 66 74 0a |hortenpr|oofleft.|
|00002120| 5c 61 64 76 61 6e 63 65 | 5c 64 69 6d 65 6e 30 2d |\advance|\dimen0-|
|00002130| 5c 73 68 6f 72 74 65 6e | 70 72 6f 6f 66 72 69 67 |\shorten|proofrig|
|00002140| 68 74 0a 25 0a 25 20 61 | 6d 6f 75 6e 74 20 6f 66 |ht.%.% a|mount of|
|00002150| 20 73 70 61 72 65 20 73 | 70 61 63 65 20 62 65 6c | spare s|pace bel|
|00002160| 6f 77 0a 5c 64 69 6d 65 | 6e 31 3d 2e 35 5c 64 69 |ow.\dime|n1=.5\di|
|00002170| 6d 65 6e 30 20 5c 61 64 | 76 61 6e 63 65 5c 64 69 |men0 \ad|vance\di|
|00002180| 6d 65 6e 31 2d 2e 35 5c | 77 64 5c 70 72 6f 6f 66 |men1-.5\|wd\proof|
|00002190| 62 65 6c 6f 77 0a 5c 64 | 69 6d 65 6e 34 3d 5c 64 |below.\d|imen4=\d|
|000021a0| 69 6d 65 6e 31 0a 5c 61 | 64 76 61 6e 63 65 5c 64 |imen1.\a|dvance\d|
|000021b0| 69 6d 65 6e 31 5c 70 72 | 6f 6f 66 62 65 6c 6f 77 |imen1\pr|oofbelow|
|000021c0| 73 68 69 66 74 20 5c 61 | 64 76 61 6e 63 65 5c 64 |shift \a|dvance\d|
|000021d0| 69 6d 65 6e 34 2d 5c 70 | 72 6f 6f 66 62 65 6c 6f |imen4-\p|roofbelo|
|000021e0| 77 73 68 69 66 74 0a 25 | 0a 25 20 63 6f 6e 63 6c |wshift.%|.% concl|
|000021f0| 75 73 69 6f 6e 20 73 74 | 69 63 6b 73 20 6f 75 74 |usion st|icks out|
|00002200| 20 74 6f 20 6c 65 66 74 | 20 6f 66 20 69 6d 6d 65 | to left| of imme|
|00002210| 64 69 61 74 65 20 68 79 | 70 6f 74 68 65 73 65 73 |diate hy|potheses|
|00002220| 0a 5c 69 66 64 69 6d 09 | 5c 64 69 6d 65 6e 31 3c |.\ifdim.|\dimen1<|
|00002230| 30 70 74 0a 5c 74 68 65 | 6e 09 5c 61 64 76 61 6e |0pt.\the|n.\advan|
|00002240| 63 65 5c 73 68 6f 72 74 | 65 6e 70 72 6f 6f 66 6c |ce\short|enproofl|
|00002250| 65 66 74 5c 64 69 6d 65 | 6e 31 0a 09 5c 61 64 76 |eft\dime|n1..\adv|
|00002260| 61 6e 63 65 5c 64 69 6d | 65 6e 30 2d 5c 64 69 6d |ance\dim|en0-\dim|
|00002270| 65 6e 31 0a 09 5c 64 69 | 6d 65 6e 31 3d 30 70 74 |en1..\di|men1=0pt|
|00002280| 0a 25 09 6e 6f 77 20 69 | 74 20 73 74 69 63 6b 73 |.%.now i|t sticks|
|00002290| 20 6f 75 74 20 74 6f 20 | 6c 65 66 74 20 6f 66 20 | out to |left of |
|000022a0| 74 72 65 65 21 0a 09 5c | 69 66 64 69 6d 20 20 5c |tree!..\|ifdim \|
|000022b0| 73 68 6f 72 74 65 6e 70 | 72 6f 6f 66 6c 65 66 74 |shortenp|roofleft|
|000022c0| 3c 30 70 74 0a 20 20 20 | 20 20 20 20 20 5c 74 68 |<0pt. | \th|
|000022d0| 65 6e 20 20 20 5c 73 65 | 74 62 6f 78 5c 70 72 6f |en \se|tbox\pro|
|000022e0| 6f 66 61 62 6f 76 65 3d | 5c 68 62 6f 78 7b 25 0a |ofabove=|\hbox{%.|
|000022f0| 09 09 09 5c 6b 65 72 6e | 2d 5c 73 68 6f 72 74 65 |...\kern|-\shorte|
|00002300| 6e 70 72 6f 6f 66 6c 65 | 66 74 5c 75 6e 68 62 6f |nproofle|ft\unhbo|
|00002310| 78 5c 70 72 6f 6f 66 61 | 62 6f 76 65 7d 25 0a 20 |x\proofa|bove}%. |
|00002320| 20 20 20 20 20 20 20 20 | 20 20 20 20 20 20 20 5c | | \|
|00002330| 73 68 6f 72 74 65 6e 70 | 72 6f 6f 66 6c 65 66 74 |shortenp|roofleft|
|00002340| 3d 30 70 74 0a 20 20 20 | 20 20 20 20 20 5c 66 69 |=0pt. | \fi|
|00002350| 0a 5c 66 69 0a 25 0a 25 | 20 61 6e 64 20 74 6f 20 |.\fi.%.%| and to |
|00002360| 74 68 65 20 72 69 67 68 | 74 0a 5c 69 66 64 69 6d |the righ|t.\ifdim|
|00002370| 09 5c 64 69 6d 65 6e 34 | 3c 30 70 74 0a 5c 74 68 |.\dimen4|<0pt.\th|
|00002380| 65 6e 09 5c 61 64 76 61 | 6e 63 65 5c 73 68 6f 72 |en.\adva|nce\shor|
|00002390| 74 65 6e 70 72 6f 6f 66 | 72 69 67 68 74 5c 64 69 |tenproof|right\di|
|000023a0| 6d 65 6e 34 0a 09 5c 61 | 64 76 61 6e 63 65 5c 64 |men4..\a|dvance\d|
|000023b0| 69 6d 65 6e 30 2d 5c 64 | 69 6d 65 6e 34 0a 09 5c |imen0-\d|imen4..\|
|000023c0| 64 69 6d 65 6e 34 3d 30 | 70 74 0a 5c 66 69 0a 25 |dimen4=0|pt.\fi.%|
|000023d0| 0a 25 20 6d 61 6b 65 20 | 73 75 72 65 20 65 6e 6f |.% make |sure eno|
|000023e0| 75 67 68 20 73 70 61 63 | 65 20 66 6f 72 20 6c 61 |ugh spac|e for la|
|000023f0| 62 65 6c 0a 5c 69 66 64 | 69 6d 09 5c 73 68 6f 72 |bel.\ifd|im.\shor|
|00002400| 74 65 6e 70 72 6f 6f 66 | 72 69 67 68 74 3c 5c 77 |tenproof|right<\w|
|00002410| 64 5c 70 72 6f 6f 66 72 | 75 6c 65 6e 61 6d 65 0a |d\proofr|ulename.|
|00002420| 5c 74 68 65 6e 09 5c 73 | 68 6f 72 74 65 6e 70 72 |\then.\s|hortenpr|
|00002430| 6f 6f 66 72 69 67 68 74 | 3d 5c 77 64 5c 70 72 6f |oofright|=\wd\pro|
|00002440| 6f 66 72 75 6c 65 6e 61 | 6d 65 0a 5c 66 69 0a 25 |ofrulena|me.\fi.%|
|00002450| 0a 25 20 63 61 6c 63 75 | 6c 61 74 65 20 6e 65 77 |.% calcu|late new|
|00002460| 20 69 6e 64 65 6e 74 61 | 74 69 6f 6e 73 0a 5c 64 | indenta|tions.\d|
|00002470| 69 6d 65 6e 32 3d 5c 73 | 68 6f 72 74 65 6e 70 72 |imen2=\s|hortenpr|
|00002480| 6f 6f 66 6c 65 66 74 20 | 5c 61 64 76 61 6e 63 65 |oofleft |\advance|
|00002490| 5c 64 69 6d 65 6e 32 20 | 62 79 5c 64 69 6d 65 6e |\dimen2 |by\dimen|
|000024a0| 31 0a 5c 64 69 6d 65 6e | 33 3d 5c 73 68 6f 72 74 |1.\dimen|3=\short|
|000024b0| 65 6e 70 72 6f 6f 66 72 | 69 67 68 74 5c 61 64 76 |enproofr|ight\adv|
|000024c0| 61 6e 63 65 5c 64 69 6d | 65 6e 33 20 62 79 5c 64 |ance\dim|en3 by\d|
|000024d0| 69 6d 65 6e 34 0a 25 0a | 25 20 6d 61 6b 65 20 74 |imen4.%.|% make t|
|000024e0| 68 65 20 72 75 6c 65 20 | 6f 72 20 64 6f 74 73 2c |he rule |or dots,|
|000024f0| 20 77 69 74 68 20 6e 61 | 6d 65 20 61 74 74 61 63 | with na|me attac|
|00002500| 68 65 64 0a 5c 69 66 70 | 72 6f 6f 66 64 6f 74 73 |hed.\ifp|roofdots|
|00002510| 0a 5c 74 68 65 6e 0a 09 | 5c 64 69 6d 65 6e 36 3d |.\then..|\dimen6=|
|00002520| 5c 73 68 6f 72 74 65 6e | 70 72 6f 6f 66 6c 65 66 |\shorten|prooflef|
|00002530| 74 20 5c 61 64 76 61 6e | 63 65 5c 64 69 6d 65 6e |t \advan|ce\dimen|
|00002540| 36 20 2e 35 5c 64 69 6d | 65 6e 30 0a 09 5c 73 65 |6 .5\dim|en0..\se|
|00002550| 74 62 6f 78 31 3d 5c 76 | 62 6f 78 20 74 6f 5c 70 |tbox1=\v|box to\p|
|00002560| 72 6f 6f 66 64 6f 74 73 | 65 70 61 72 61 74 69 6f |roofdots|eparatio|
|00002570| 6e 7b 5c 76 73 73 5c 68 | 62 6f 78 7b 24 5c 63 64 |n{\vss\h|box{$\cd|
|00002580| 6f 74 24 7d 5c 76 73 73 | 7d 0a 09 5c 73 65 74 62 |ot$}\vss|}..\setb|
|00002590| 6f 78 30 3d 5c 68 62 6f | 78 7b 25 0a 09 09 5c 6b |ox0=\hbo|x{%...\k|
|000025a0| 65 72 6e 5c 64 69 6d 65 | 6e 36 0a 09 09 24 5c 76 |ern\dime|n6...$\v|
|000025b0| 63 65 6e 74 65 72 20 74 | 6f 5c 70 72 6f 6f 66 64 |center t|o\proofd|
|000025c0| 6f 74 6e 75 6d 62 65 72 | 5c 70 72 6f 6f 66 64 6f |otnumber|\proofdo|
|000025d0| 74 73 65 70 61 72 61 74 | 69 6f 6e 0a 09 09 09 7b |tseparat|ion....{|
|000025e0| 5c 6c 65 61 64 65 72 73 | 5c 62 6f 78 31 5c 76 66 |\leaders|\box1\vf|
|000025f0| 69 6c 6c 7d 24 25 0a 09 | 09 5c 75 6e 68 62 6f 78 |ill}$%..|.\unhbox|
|00002600| 5c 70 72 6f 6f 66 72 75 | 6c 65 6e 61 6d 65 7d 25 |\proofru|lename}%|
|00002610| 0a 5c 65 6c 73 65 09 5c | 64 69 6d 65 6e 36 3d 5c |.\else.\|dimen6=\|
|00002620| 66 6f 6e 74 64 69 6d 65 | 6e 32 32 5c 74 68 65 5c |fontdime|n22\the\|
|00002630| 74 65 78 74 66 6f 6e 74 | 32 20 25 20 68 65 69 67 |textfont|2 % heig|
|00002640| 68 74 20 6f 66 20 6d 61 | 74 68 73 20 61 78 69 73 |ht of ma|ths axis|
|00002650| 0a 09 5c 64 69 6d 65 6e | 37 3d 5c 64 69 6d 65 6e |..\dimen|7=\dimen|
|00002660| 36 0a 09 5c 61 64 76 61 | 6e 63 65 5c 64 69 6d 65 |6..\adva|nce\dime|
|00002670| 6e 36 62 79 2e 35 5c 70 | 72 6f 6f 66 72 75 6c 65 |n6by.5\p|roofrule|
|00002680| 62 72 65 61 64 74 68 0a | 09 5c 61 64 76 61 6e 63 |breadth.|.\advanc|
|00002690| 65 5c 64 69 6d 65 6e 37 | 62 79 2d 2e 35 5c 70 72 |e\dimen7|by-.5\pr|
|000026a0| 6f 6f 66 72 75 6c 65 62 | 72 65 61 64 74 68 0a 09 |oofruleb|readth..|
|000026b0| 5c 73 65 74 62 6f 78 30 | 3d 5c 68 62 6f 78 7b 25 |\setbox0|=\hbox{%|
|000026c0| 0a 09 09 5c 6b 65 72 6e | 5c 73 68 6f 72 74 65 6e |...\kern|\shorten|
|000026d0| 70 72 6f 6f 66 6c 65 66 | 74 0a 09 09 5c 69 66 64 |prooflef|t...\ifd|
|000026e0| 6f 75 62 6c 65 70 72 6f | 6f 66 0a 09 09 5c 74 68 |oublepro|of...\th|
|000026f0| 65 6e 09 5c 68 62 6f 78 | 20 74 6f 5c 64 69 6d 65 |en.\hbox| to\dime|
|00002700| 6e 30 7b 25 0a 09 09 09 | 24 5c 6d 61 74 68 73 75 |n0{%....|$\mathsu|
|00002710| 72 72 6f 75 6e 64 30 70 | 74 5c 6d 61 74 68 6f 72 |rround0p|t\mathor|
|00002720| 64 3d 5c 6d 6b 65 72 6e | 2d 36 6d 75 25 0a 09 09 |d=\mkern|-6mu%...|
|00002730| 09 5c 63 6c 65 61 64 65 | 72 73 5c 68 62 6f 78 7b |.\cleade|rs\hbox{|
|00002740| 24 5c 6d 6b 65 72 6e 2d | 32 6d 75 3d 5c 6d 6b 65 |$\mkern-|2mu=\mke|
|00002750| 72 6e 2d 32 6d 75 24 7d | 5c 68 66 69 6c 6c 0a 09 |rn-2mu$}|\hfill..|
|00002760| 09 09 5c 6d 6b 65 72 6e | 2d 36 6d 75 5c 6d 61 74 |..\mkern|-6mu\mat|
|00002770| 68 6f 72 64 3d 24 7d 25 | 0a 09 09 5c 65 6c 73 65 |hord=$}%|...\else|
|00002780| 09 5c 76 72 75 6c 65 20 | 68 65 69 67 68 74 5c 64 |.\vrule |height\d|
|00002790| 69 6d 65 6e 36 20 64 65 | 70 74 68 2d 5c 64 69 6d |imen6 de|pth-\dim|
|000027a0| 65 6e 37 20 77 69 64 74 | 68 5c 64 69 6d 65 6e 30 |en7 widt|h\dimen0|
|000027b0| 0a 09 09 5c 66 69 0a 09 | 09 5c 75 6e 68 62 6f 78 |...\fi..|.\unhbox|
|000027c0| 5c 70 72 6f 6f 66 72 75 | 6c 65 6e 61 6d 65 7d 25 |\proofru|lename}%|
|000027d0| 0a 09 5c 68 74 30 3d 5c | 64 69 6d 65 6e 36 20 5c |..\ht0=\|dimen6 \|
|000027e0| 64 70 30 3d 2d 5c 64 69 | 6d 65 6e 37 0a 5c 66 69 |dp0=-\di|men7.\fi|
|000027f0| 0a 25 0a 25 20 73 65 74 | 20 75 70 20 74 6f 20 63 |.%.% set| up to c|
|00002800| 65 6e 74 72 65 20 6f 75 | 74 65 72 6d 6f 73 74 20 |entre ou|termost |
|00002810| 74 72 65 65 20 6f 6e 6c | 79 0a 5c 6c 65 74 5c 64 |tree onl|y.\let\d|
|00002820| 6f 6c 6c 5c 72 65 6c 61 | 78 0a 5c 69 66 77 61 73 |oll\rela|x.\ifwas|
|00002830| 69 6e 73 69 64 65 70 72 | 6f 6f 66 74 72 65 65 0a |insidepr|ooftree.|
|00002840| 5c 74 68 65 6e 09 5c 6c | 65 74 5c 56 42 4f 58 5c |\then.\l|et\VBOX\|
|00002850| 76 62 6f 78 0a 5c 65 6c | 73 65 09 5c 69 66 6d 6d |vbox.\el|se.\ifmm|
|00002860| 6f 64 65 5c 65 6c 73 65 | 24 5c 6c 65 74 5c 64 6f |ode\else|$\let\do|
|00002870| 6c 6c 3d 24 5c 66 69 0a | 09 5c 6c 65 74 5c 56 42 |ll=$\fi.|.\let\VB|
|00002880| 4f 58 5c 76 63 65 6e 74 | 65 72 0a 5c 66 69 0a 25 |OX\vcent|er.\fi.%|
|00002890| 20 74 68 69 73 20 5c 76 | 62 6f 78 20 6f 72 20 5c | this \v|box or \|
|000028a0| 76 63 65 6e 74 65 72 20 | 69 73 20 74 68 65 20 61 |vcenter |is the a|
|000028b0| 63 74 75 61 6c 20 6f 75 | 74 70 75 74 3a 0a 5c 56 |ctual ou|tput:.\V|
|000028c0| 42 4f 58 09 7b 5c 62 61 | 73 65 6c 69 6e 65 73 6b |BOX.{\ba|selinesk|
|000028d0| 69 70 5c 70 72 6f 6f 66 | 72 75 6c 65 62 61 73 65 |ip\proof|rulebase|
|000028e0| 6c 69 6e 65 20 5c 6c 69 | 6e 65 73 6b 69 70 2e 32 |line \li|neskip.2|
|000028f0| 65 78 0a 09 5c 65 78 70 | 61 6e 64 61 66 74 65 72 |ex..\exp|andafter|
|00002900| 5c 6c 69 6e 65 73 6b 69 | 70 6c 69 6d 69 74 5c 69 |\lineski|plimit\i|
|00002910| 66 70 72 6f 6f 66 64 6f | 74 73 30 65 78 5c 65 6c |fproofdo|ts0ex\el|
|00002920| 73 65 2d 30 2e 36 65 78 | 5c 66 69 0a 09 5c 68 62 |se-0.6ex|\fi..\hb|
|00002930| 6f 78 09 73 70 72 65 61 | 64 5c 64 69 6d 65 6e 35 |ox.sprea|d\dimen5|
|00002940| 09 7b 5c 68 66 69 5c 75 | 6e 68 62 6f 78 5c 70 72 |.{\hfi\u|nhbox\pr|
|00002950| 6f 6f 66 61 62 6f 76 65 | 5c 68 66 69 7d 25 0a 09 |oofabove|\hfi}%..|
|00002960| 5c 68 62 6f 78 7b 5c 62 | 6f 78 30 7d 25 0a 09 5c |\hbox{\b|ox0}%..\|
|00002970| 68 62 6f 78 09 7b 5c 6b | 65 72 6e 5c 64 69 6d 65 |hbox.{\k|ern\dime|
|00002980| 6e 32 20 5c 62 6f 78 5c | 70 72 6f 6f 66 62 65 6c |n2 \box\|proofbel|
|00002990| 6f 77 7d 7d 5c 64 6f 6c | 6c 25 0a 25 0a 25 20 70 |ow}}\dol|l%.%.% p|
|000029a0| 61 73 73 20 6e 65 77 20 | 69 6e 64 65 6e 74 61 74 |ass new |indentat|
|000029b0| 69 6f 6e 73 20 6f 75 74 | 20 6f 66 20 73 63 6f 70 |ions out| of scop|
|000029c0| 65 0a 5c 67 6c 6f 62 61 | 6c 5c 64 69 6d 65 6e 32 |e.\globa|l\dimen2|
|000029d0| 3d 5c 64 69 6d 65 6e 32 | 0a 5c 67 6c 6f 62 61 6c |=\dimen2|.\global|
|000029e0| 5c 64 69 6d 65 6e 33 3d | 5c 64 69 6d 65 6e 33 0a |\dimen3=|\dimen3.|
|000029f0| 5c 65 67 72 6f 75 70 20 | 25 20 4e 45 53 54 45 44 |\egroup |% NESTED|
|00002a00| 20 5a 45 52 4f 0a 5c 69 | 66 6f 6e 6c 65 66 74 6f | ZERO.\i|fonlefto|
|00002a10| 66 70 72 6f 6f 66 72 75 | 6c 65 0a 5c 74 68 65 6e |fproofru|le.\then|
|00002a20| 09 5c 73 68 6f 72 74 65 | 6e 70 72 6f 6f 66 6c 65 |.\shorte|nproofle|
|00002a30| 66 74 3d 5c 64 69 6d 65 | 6e 32 0a 5c 66 69 0a 5c |ft=\dime|n2.\fi.\|
|00002a40| 73 68 6f 72 74 65 6e 70 | 72 6f 6f 66 72 69 67 68 |shortenp|roofrigh|
|00002a50| 74 3d 5c 64 69 6d 65 6e | 33 0a 25 0a 25 20 73 6f |t=\dimen|3.%.% so|
|00002a60| 6d 65 20 73 70 61 63 65 | 20 6f 6e 20 72 69 67 68 |me space| on righ|
|00002a70| 74 20 61 6e 64 20 66 6c | 61 67 20 77 65 27 76 65 |t and fl|ag we've|
|00002a80| 20 6a 75 73 74 20 6d 61 | 64 65 20 61 20 74 72 65 | just ma|de a tre|
|00002a90| 65 0a 5c 6f 6e 6c 65 66 | 74 6f 66 70 72 6f 6f 66 |e.\onlef|tofproof|
|00002aa0| 72 75 6c 65 66 61 6c 73 | 65 0a 5c 69 66 69 6e 73 |rulefals|e.\ifins|
|00002ab0| 69 64 65 70 72 6f 6f 66 | 74 72 65 65 0a 5c 74 68 |ideproof|tree.\th|
|00002ac0| 65 6e 09 5c 68 73 6b 69 | 70 2e 35 65 6d 20 70 6c |en.\hski|p.5em pl|
|00002ad0| 75 73 20 31 66 69 6c 20 | 5c 70 65 6e 61 6c 74 79 |us 1fil |\penalty|
|00002ae0| 32 0a 5c 66 69 0a 7d 0a | 0a 25 3d 3d 3d 3d 3d 3d |2.\fi.}.|.%======|
|00002af0| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00002b00| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00002b10| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00002b20| 3d 3d 3d 3d 3d 3d 3d 3d | 3d 3d 3d 3d 3d 3d 3d 3d |========|========|
|00002b30| 3d 3d 3d 3d 0a 25 20 49 | 44 45 41 53 0a 25 20 31 |====.% I|DEAS.% 1|
|00002b40| 2e 09 53 70 65 63 69 66 | 69 63 61 74 69 6f 6e 20 |..Specif|ication |
|00002b50| 6f 66 20 5c 73 68 69 66 | 74 72 69 67 68 74 20 61 |of \shif|tright a|
|00002b60| 6e 64 20 68 6f 77 20 74 | 6f 20 73 70 72 65 61 64 |nd how t|o spread|
|00002b70| 20 74 72 65 65 73 2e 0a | 25 20 32 2e 09 53 70 61 | trees..|% 2..Spa|
|00002b80| 63 69 6e 67 20 63 6f 6d | 6d 61 6e 64 20 5c 6d 20 |cing com|mand \m |
|00002b90| 77 68 69 63 68 20 63 61 | 75 73 65 73 20 31 65 6d |which ca|uses 1em|
|00002ba0| 2b 31 66 69 6c 20 73 70 | 61 63 69 6e 67 2c 20 6f |+1fil sp|acing, o|
|00002bb0| 76 65 72 2d 72 69 64 69 | 6e 67 0a 25 09 65 78 69 |ver-ridi|ng.%.exi|
|00002bc0| 73 69 74 69 6e 67 20 73 | 70 61 63 65 20 6f 6e 20 |siting s|pace on |
|00002bd0| 73 69 64 65 73 20 6f 66 | 20 74 72 65 65 73 20 61 |sides of| trees a|
|00002be0| 6e 64 20 6e 6f 74 20 61 | 66 66 65 63 74 69 6e 67 |nd not a|ffecting|
|00002bf0| 20 74 68 65 0a 25 09 64 | 65 74 65 63 74 69 6f 6e | the.%.d|etection|
|00002c00| 20 6f 66 20 62 65 69 6e | 67 20 6f 6e 20 74 68 65 | of bein|g on the|
|00002c10| 20 6c 65 66 74 20 6f 72 | 20 72 69 67 68 74 2e 0a | left or| right..|
|00002c20| 25 20 33 2e 09 48 61 63 | 6b 20 75 73 69 6e 67 20 |% 3..Hac|k using |
|00002c30| 5c 40 63 75 72 72 65 6e | 76 69 72 20 74 6f 20 64 |\@curren|vir to d|
|00002c40| 65 74 65 63 74 20 4c 61 | 54 65 58 20 65 6e 76 69 |etect La|TeX envi|
|00002c50| 72 6f 6e 6d 65 6e 74 3b | 20 68 61 76 65 20 74 6f |ronment;| have to|
|00002c60| 0a 25 09 75 73 65 20 5c | 61 66 74 65 72 67 72 6f |.%.use \|aftergro|
|00002c70| 75 70 20 74 6f 20 70 61 | 73 73 20 5c 73 68 6f 72 |up to pa|ss \shor|
|00002c80| 74 65 6e 70 72 6f 6f 66 | 6c 65 66 74 2f 72 69 67 |tenproof|left/rig|
|00002c90| 68 74 20 6f 75 74 2e 0a | 25 20 34 2e 09 28 50 69 |ht out..|% 4..(Pi|
|00002ca0| 65 20 69 6e 20 74 68 65 | 20 73 6b 79 29 20 64 65 |e in the| sky) de|
|00002cb0| 74 65 63 74 20 68 6f 77 | 20 6d 75 63 68 20 74 72 |tect how| much tr|
|00002cc0| 65 65 73 20 63 61 6e 20 | 62 65 20 22 74 75 63 6b |ees can |be "tuck|
|00002cd0| 65 64 20 69 6e 22 0a 25 | 20 35 2e 09 44 69 73 63 |ed in".%| 5..Disc|
|00002ce0| 68 61 72 67 65 64 20 68 | 79 70 6f 74 68 65 73 65 |harged h|ypothese|
|00002cf0| 73 20 28 64 69 61 67 6f | 6e 61 6c 20 6c 69 6e 65 |s (diago|nal line|
|00002d00| 73 29 2e 0a | |s).. | |
+--------+-------------------------+-------------------------+--------+--------+
